;;;
;;; preprocessing.lisp: Preprocessing for Resolution Theorem Proving
;;;
;;; Utility functions for performing the 7 preprocessing steps specified
;;; in lecture 20.
;;;

;;
;; Step 1: Eliminate Implications
;;

(defun eliminate-implications (wff)
  "Given a WFF, return an equivalent formula without implications."
  (cond
   ((equivalence-p wff)
    (let ((wff1 (eliminate-implications (equivalence-wff1 wff)))
	  (wff2 (eliminate-implications (equivalence-wff2 wff))))
      (make-conjunction (make-reduced-implication wff1 wff2)
			(make-reduced-implication wff2 wff1))))
   ((implication-p wff)
    (let ((wff1 (eliminate-implications (implication-wff1 wff)))
	  (wff2 (eliminate-implications (implication-wff2 wff))))
      (make-reduced-implication wff1 wff2)))
   ((negation-p wff)
    (make-negation (eliminate-implications (negation-wff wff))))
   ((disjunction-p wff)
    (make-disjunction (eliminate-implications (disjunction-wff1 wff))
		      (eliminate-implications (disjunction-wff2 wff))))
   ((conjunction-p wff)
    (make-conjunction (eliminate-implications (conjunction-wff1 wff))
		      (eliminate-implications (conjunction-wff2 wff))))
   ((universal-p wff)
    (make-universal (universal-var wff) 
		    (eliminate-implications (universal-wff wff))))
   ((existential-p wff)
    (make-existential (existential-var wff)
		      (eliminate-implications (existential-wff wff))))
   (t wff)))

(defun make-reduced-implication (wff1 wff2)
  (make-disjunction (make-negation wff1) wff2))

;;
;; Step 2: Move Negation Inwards
;;

(defun move-negations-inwards (wff)
  "Given a WFF without implications, return an equivalent formula
in negation normal form."
  (cond
   ((negation-p wff)
    (let ((negated-wff (move-negations-inwards (negation-wff wff))))
      (cond
       ((negation-p negated-wff)
	(move-negations-inwards (negation-wff negated-wff)))
       ((disjunction-p negated-wff)
	(make-conjunction 
	 (move-negations-inwards 
	  (make-negation (disjunction-wff1 negated-wff)))
	 (move-negations-inwards 
	  (make-negation (disjunction-wff2 negated-wff)))))
       ((conjunction-p negated-wff)
	(make-disjunction 
	 (move-negations-inwards
	  (make-negation (conjunction-wff1 negated-wff)))
	 (move-negations-inwards
	  (make-negation (conjunction-wff2 negated-wff)))))
       ((universal-p negated-wff)
	(make-existential (universal-var negated-wff)
			  (move-negations-inwards
			   (make-negation (universal-wff negated-wff)))))
       ((existential-p negated-wff)
	(make-universal (existential-var negated-wff)
			(move-negations-inwards
			 (make-negation (existential-wff negated-wff)))))
       (t (make-negation negated-wff)))))
   ((disjunction-p wff)
    (make-disjunction (move-negations-inwards (disjunction-wff1 wff))
		      (move-negations-inwards (disjunction-wff2 wff))))
   ((conjunction-p wff)
    (make-conjunction (move-negations-inwards (conjunction-wff1 wff))
		      (move-negations-inwards (conjunction-wff2 wff))))
   ((universal-p wff)
    (make-universal (universal-var wff) 
		    (move-negations-inwards (universal-wff wff))))
   ((existential-p wff)
    (make-existential (existential-var wff)
		      (move-negations-inwards (existential-wff wff))))
   (t wff)))

;;
;; Step 3: Standardize Variables
;;

(defun standardize-variables (wff)
  "Given a negation-normal form formula WFF with implications eliminated,
return a semantically equivalent formula with all quantified variables
standardized apart."
  (cond
   ((negation-p wff)
    (make-negation (standardize-variables (negation-wff wff))))
   ((disjunction-p wff)
    (make-disjunction (standardize-variables (disjunction-wff1 wff))
		      (standardize-variables (disjunction-wff2 wff))))
   ((conjunction-p wff)
    (make-conjunction (standardize-variables (conjunction-wff1 wff))
		      (standardize-variables (conjunction-wff2 wff))))
   ((universal-p wff)
    (let ((new-var (make-fresh-variable))
	  (old-var (universal-var wff))
	  (body    (universal-wff wff)))
      (make-universal new-var
		      (standardize-variables (wff-substitute body old-var 
							     new-var)))))
   ((existential-p wff)
    (let ((new-var (make-fresh-variable))
	  (old-var (existential-var wff))
	  (body    (existential-wff wff)))
      (make-existential new-var
			(standardize-variables (wff-substitute body old-var
							       new-var)))))
   (t wff)))


;;
;; Step 4: Move Quantifiers Left
;;

(defun move-quantifiers-left (wff)
  "Given a negation normal form formula WFF with no implications and with 
quantified variables standardized apart, convert it to an equivalent prenex 
normal form formula."
  (cond
   ((universal-p wff) 
    (make-universal (universal-var wff)
		    (move-quantifiers-left (universal-wff wff))))
   ((existential-p wff)
    (make-existential (existential-var wff)
		      (move-quantifiers-left (existential-wff wff))))
   ((conjunction-p wff)
    (let ((wff1 (move-quantifiers-left (conjunction-wff1 wff)))
	  (wff2 (move-quantifiers-left (conjunction-wff2 wff))))
      (make-mql-reduced-conjunction wff1 wff2)))
   ((disjunction-p wff)
    (let ((wff1 (move-quantifiers-left (disjunction-wff1 wff)))
	  (wff2 (move-quantifiers-left (disjunction-wff2 wff))))
      (make-mql-reduced-disjunction wff1 wff2)))
   (t wff)))

(defun make-mql-reduced-conjunction (wff1 wff2)
  (cond
   ((existential-p wff1)
    (make-existential (existential-var wff1)
		      (make-mql-reduced-conjunction (existential-wff wff1)
						    wff2)))
   ((existential-p wff2)
    (make-existential (existential-var wff2)
		      (make-mql-reduced-conjunction wff1
						    (existential-wff wff2))))
   ((universal-p wff1) 
    (make-universal (universal-var wff1)
		    (make-mql-reduced-conjunction (universal-wff wff1)
						  wff2)))
   ((universal-p wff2)
    (make-universal (universal-var wff2)
		    (make-mql-reduced-conjunction wff1
						  (universal-wff wff2))))
   (t (make-conjunction wff1 wff2))))

(defun make-mql-reduced-disjunction (wff1 wff2)
  (cond
   ((existential-p wff1)
    (make-existential (existential-var wff1)
		      (make-mql-reduced-disjunction (existential-wff wff1)
						    wff2)))
   ((existential-p wff2)
    (make-existential (existential-var wff2)
		      (make-mql-reduced-disjunction wff1
						    (existential-wff wff2))))
   ((universal-p wff1)
    (make-universal (universal-var wff1)
		    (make-mql-reduced-disjunction (universal-wff wff1)
						  wff2)))
   ((universal-p wff2)
    (make-universal (universal-var wff1)
		    (make-mql-reduced-disjunction wff1
						  (universal-wff wff2))))
   (t (make-disjunction wff1 wff2))))

;;
;; Step 5: Skolemize
;;

(defun generate-skolem-function (var-list)
  "Given a list VAR-LIST of variables, return a fresh Skolem function
with the variables in VAR-LIST as arguments.  The function symbol for
the returned Skolem function is guaranteed to be unique system wide."
  (cons (gentemp "SKOLEM-FUNC-") var-list))

(defun skolemize (wff)
  "Given a formula WFF with implications eliminated, negations moved inwards,
variables standized apart, and in Prenex Normal Form, convert the formula
into Skolem Standard Form.  Skolem constants are represented as Skolem
functions with no argument."
  ;;
  ;; You fill out the detail here...
  ;;
)

;; 
;; Step 6: Distribute disjunctions over conjunction
;;

(defun distribute-disj-over-conj (wff)
  "Given a formula WFF in Skolem Standard Form, return an equivalent
formula with disjunctions distributed over conjunctions."
  (cond
   ((universal-p wff) 
    (make-universal (universal-var wff) 
		    (distribute-disj-over-conj (universal-wff wff))))
   ((conjunction-p wff)
    (let ((wff1 (distribute-disj-over-conj (conjunction-wff1 wff)))
	  (wff2 (distribute-disj-over-conj (conjunction-wff2 wff))))
      (make-ddoc-reduced-conjunction wff1 wff2)))
   ((disjunction-p wff)
    (let ((wff1 (distribute-disj-over-conj (disjunction-wff1 wff)))
	  (wff2 (distribute-disj-over-conj (disjunction-wff2 wff))))
      (make-ddoc-reduced-disjunction wff1 wff2)))
   (t wff)))

(defun make-ddoc-reduced-conjunction (wff1 wff2)
  (make-conjunction wff1 wff2))

(defun make-ddoc-reduced-disjunction (wff1 wff2)
  (cond
   ((conjunction-p wff1) 
    (make-conjunction (make-ddoc-reduced-disjunction (conjunction-wff1 wff1)
						     wff2)
		      (make-ddoc-reduced-disjunction (conjunction-wff2 wff1)
						     wff2)))
   ((conjunction-p wff2)
    (make-conjunction (make-ddoc-reduced-disjunction wff1
						     (conjunction-wff1 wff2))
		      (make-ddoc-reduced-disjunction wff1
						     (conjunction-wff2 wff2))))
   (t (make-disjunction wff1 wff2))))

;;
;; Step 7: Convert to Clausal Form
;;

(defun clausal-form (wff)
  "Given a WFF in Skolem Standard Form so that its matrix is in CNF, return 
its clausal form representation."
  (flatten-conjunction (extract-matrix wff)))

(defun extract-matrix (wff)
  (if (universal-p wff)
      (extract-matrix (universal-wff wff))
    wff))

(defun flatten-conjunction (wff)
  (if (conjunction-p wff)
      (append (flatten-conjunction (conjunction-wff1 wff))
	      (flatten-conjunction (conjunction-wff2 wff)))
    (list (flatten-disjunction wff))))

(defun flatten-disjunction (wff)
  (if (disjunction-p wff)
      (append (flatten-disjunction (disjunction-wff1 wff))
	      (flatten-disjunction (disjunction-wff2 wff)))
    (list wff)))

